(module manifest (lib "eopl.ss" "eopl")

  (require "lang.scm")
  (require "static-data-structures.scm")
  (require "expand-type.scm")

  (provide module-definitions->manifest)

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;; manifests
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  ;;; A manifest is just a type environment.  We build the
  ;;; manifest in two stages:  First we build a type environment
  ;;; consisting of all the module definitions.  Then we build a
  ;;; second type environment just like the first, except that all the
  ;;; types are expanded.  This process is idempotent, so we only have
  ;;; to do it once.  After that, all the types are canonical:  any
  ;;; qualified type or module type that appears in a type environment
  ;;; will already be expanded.  Need to make sure that this invariant
  ;;; is enforced.

  ;; we need this so that we don't have to import a module just to see
  ;; the types.  It's perfectly fine for from m1 take t to match from
  ;; m1 take t, even if m1 isn't imported (!).

  (define module-definitions->manifest
    (lambda (defns)
      (build-expanded-manifest defns
        (build-primitive-manifest defns))))

  (define build-primitive-manifest
    (lambda (defns)
      (if (null? defns) 
        (empty-tenv)
        (extend-tenv-with-module
          (module-definition->name (car defns))
          (module-definition->module-type (car defns))
          (build-primitive-manifest (cdr defns))))))

  (define build-expanded-manifest
    (lambda (defns tenv)
      (let recur ((defns defns))
        (if (null? defns) 
          (empty-tenv)
          (extend-tenv-with-module
            (module-definition->name (car defns))
            (expand-module-type-in-tenv
              (module-definition->module-type (car defns))
              tenv)
            (recur (cdr defns)))))))

;;  (trace build-expanded-manifest)
  
  )